Termination w.r.t. Q proof of /tmp/tmpAlWdy9/thiemann03.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

SHUFF(x, y) → HEAD(x)
REVERSE(add(n, x)) → REVERSE(x)
REVERSE(add(n, x)) → APP(reverse(x), add(n, nil))
APP(add(n, x), y) → APP(x, y)
SHUFFLE(x) → SHUFF(x, nil)
IF(false, x, y, z) → TAIL(x)
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
IF(false, x, y, z) → REVERSE(tail(x))
SHUFF(x, y) → NULL(x)
SHUFF(x, y) → APP(y, add(head(x), nil))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(x, y) → HEAD(x)
REVERSE(add(n, x)) → REVERSE(x)
REVERSE(add(n, x)) → APP(reverse(x), add(n, nil))
APP(add(n, x), y) → APP(x, y)
SHUFFLE(x) → SHUFF(x, nil)
IF(false, x, y, z) → TAIL(x)
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
IF(false, x, y, z) → REVERSE(tail(x))
SHUFF(x, y) → NULL(x)
SHUFF(x, y) → APP(y, add(head(x), nil))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 7 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP(add(n, x), y) → APP(x, y)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE(add(n, x)) → REVERSE(x)

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE(add(n, x)) → REVERSE(x)

R is empty.
The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE(add(n, x)) → REVERSE(x)

From the DPs we obtained the following set of size-change graphs:

REVERSE(add(n, x)) → REVERSE(x)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil))) at position [0] we obtained the following new rules:

SHUFF(nil, y1) → IF(true, nil, y1, app(y1, add(head(nil), nil)))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(nil, y1) → IF(true, nil, y1, app(y1, add(head(nil), nil)))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))

The TRS R consists of the following rules:

null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))

The TRS R consists of the following rules:

head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

null(nil)
null(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))

The TRS R consists of the following rules:

head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil))) at position [3,1,0] we obtained the following new rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)

The TRS R consists of the following rules:

head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)

The TRS R consists of the following rules:

app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

head(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)

The TRS R consists of the following rules:

app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule IF(false, x, y, z) → SHUFF(reverse(tail(x)), z) at position [0] we obtained the following new rules:

IF(false, nil, y1, y2) → SHUFF(reverse(nil), y2)
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, nil, y1, y2) → SHUFF(reverse(nil), y2)
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

The TRS R consists of the following rules:

app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

The TRS R consists of the following rules:

app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

The TRS R consists of the following rules:

reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))

The set Q consists of the following terms:

tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

tail(add(x0, x1))
tail(nil)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

The TRS R consists of the following rules:

reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))

The set Q consists of the following terms:

app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)

The remaining pairs can at least be oriented weakly.

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))

Used ordering: Polynomial interpretation [25]:

POL(IF(x₁, x₂, x₃, x₄)) = x₂
POL(SHUFF(x₁, x₂)) = x₁
POL(add(x₁, x₂)) = 1 + x₁ + x₂
POL(app(x₁, x₂)) = x₁ + x₂
POL(false) = 0
POL(nil) = 0
POL(reverse(x₁)) = x₁

The following usable rules [17] were oriented:

app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
reverse(nil) → nil

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Rewriting

                                          ↳ QDP

                                            ↳ UsableRulesProof

                                              ↳ QDP

                                                ↳ QReductionProof

                                                  ↳ QDP

                                                    ↳ Narrowing

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ UsableRulesProof

                                                              ↳ QDP

                                                                ↳ QReductionProof

                                                                  ↳ QDP

                                                                    ↳ QDPOrderProof

                                                                      ↳ QDP

                                                                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))

The TRS R consists of the following rules:

reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))

The set Q consists of the following terms:

app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.